/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.semantic;

import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.Set;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Expr;
import alloy.ast.FindCommand;
import alloy.ast.Module;
import alloy.ast.UnaryExpr;
import alloy.ast.UnaryExprOp;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.type.SigType;
import alloy.type.UnionType;

/**
 * This visitor can be applied to only to a typechecked AST subtree rooted at
 * a Specification, Modules, or Module node.  All the commands must be desugared
 * and converted into formulas before this visitor is called.
 * For each command in the AST subtree, it detects all BasicTypes in the command's formula 
 * that have a closure operator applied to them and calls the setClosedTypes
 * method of the Module's ModuleInfo with the set containing the detected 
 * types.
 **/
public class ClosedTypesDetectionVisitor extends ASTDepthFirstVisitor {

    /** contains the closed types for the current module **/
    private Set _closedTypes;

    private TypeErrorReporter _err = new TypeErrorReporter();

    /** Visit a node of type {@link Module}
     *  and traverse its children depth first*/
    public void visit(Module module_){

	// if module does not contain any commands,
	// do nothing
	if (!module_.getCommands().getCommandIter().hasNext())
	    return;

	// initialize _closedTypes
	_closedTypes = new HashSet();

	// fill _closedTypes
	module_.getCommands().applyVisitor(this);



	// set ModuleInfo's closedTypes to computed _closedTypes
	module_.getModuleInfo().setClosedTypes(_closedTypes);

    }
    
    public void visit(FindCommand command_) {
	// we detect closed types in the command_'s formula ...
	command_.formula.applyVisitor(this);
    }

    /**
     * @return an Iterator that contains a path from bt to the top of the hierarchy
     * tree to which bt belongs.  The first element of returned by the iterator is the
     * root of the hierarchy.  For example if A extends B which extends C, 
     * applying getPathToRoot to A would result in an iterator that returns
     * C, B, and A, in that order.
     **/
    private static Iterator getPathToRoot(BasicType bt) {
	LinkedList path = new LinkedList();

	if (bt.isEmpty()) {
	    path.add(bt);
	} else {

	    SigType stCur = (SigType) bt;
	    while (stCur != null) {
		path.addFirst(stCur);
		stCur = stCur.getSuperType();
	    }
	}
	
	return path.iterator();
    }


    /**
     * @return a BasicType bt' such that bt1.isSubtypeOf(bt') && bt2.isSubtypeOf(bt') &&
     * there is no bt'' != bt' such that bt''.isSubtypeOf(bt') && bt1.isSubtypeOf(bt'') && 
     * bt2.isSubtypeOf(bt'').  If no such bt' exists, null is returned.
     **/
    private static BasicType getLeastCommonSuperType(BasicType bt1, BasicType bt2) {
	Iterator p1Iter = getPathToRoot(bt1);
	Iterator p2Iter = getPathToRoot(bt2);
	
	BasicType lcst = null;

	while (p1Iter.hasNext() && p2Iter.hasNext()) {
	    BasicType p1bt = (BasicType) p1Iter.next();
	    BasicType p2bt = (BasicType) p2Iter.next();
	    if (p1bt.equals(p2bt))
		lcst = p1bt;
	    else
		break;
	}

	return lcst;
    }

    /**
     * adds bt to _closedTypes if _closedTypes does not already
     * contain bt or its supertype
     **/
    private void addToClosedTypes(BasicType bt) {
	for (Iterator ctIter = _closedTypes.iterator(); ctIter.hasNext(); ) {
	    BasicType btCur = (BasicType) ctIter.next();
	    if (bt.isSubtypeOf(btCur))
		return;
	    if (btCur.isSubtypeOf(bt))
		ctIter.remove();
	}
	_closedTypes.add(bt);
    }

    /** Visit a node of type {@link UnaryExpr}
     *  and traverse its children depth first*/
    public void visit(UnaryExpr unaryExpr_) {
	
	if (unaryExpr_.getOp().equals(UnaryExprOp.TRANSPOSE)) {
	    // nothing to do for transpose
	    return;
	}
	
	Expr expr = unaryExpr_.getExpr();
	UnionType exprType = expr.getType();

	// contains RelationTypes in exprType that cannot be squared
	Set nonSquare = new HashSet();
	
	// examine each RelationType in exprType; if it can be squared,
	// add it to the _closedTypes.  If not, add it to nonSquare
	for (Iterator rtIter = exprType.getTypeIter(); rtIter.hasNext(); ) {
	    RelationType rt = (RelationType) rtIter.next();
	    BasicType bt = getLeastCommonSuperType(rt.getBasicTypeAt(0),
						   rt.getBasicTypeAt(1));
	    // rt cannot be squared, add it to nonSquare 
	    if (bt == null) {
		nonSquare.add(rt);
	    } else { // add bt to _closedTypes
		addToClosedTypes(bt);
	    }
	}
	
	// if there are any non square components in exprType, signal an error
	if (!nonSquare.isEmpty()) {
	    _err.type("closure expression has square type.\n" +
		      TypeErrorReporter.format(expr) + 
		      "\nNon-square components: " + nonSquare.toString(), expr);
	}

	expr.applyVisitor(this);

    }


    
}
